$\forall$$T$:Type, ${\it dT}$:EqDecider($T$), $L$:$T$ List, $x$:$T$. ($x$ $\in$ $L$) $\Rightarrow$ index($L$;$x$) $\in$ $\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$